COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSP.PUB[206,CLT]" source_file
C00003 00003	.bb Informal description of a possible solution to the "component of a graph" problem.
C00008 00004	.bb Revised description of a possible solution to the "component of a graph" problem.
C00012 ENDMK
C⊗;
.REQUIRE "LSP.PUB[206,CLT]" source_file;
.
.lspfont
.basicops
.
.PORTION MAINPORTION
.
.page←1
.bb Informal description of a possible solution to the "component of a graph" problem.

	Assume the function ⊗successors represents a finite graph G.  We
introduce a sort ⊗isvertex intended to test if an individual is a vertex
in G, and let the variables ⊗a, ⊗b, ⊗c ... range over vertices of G.  We
define some predicates useful in discussing graphs.

⊗⊗∀a b u: [path[a, b, u] ≡ ¬qn u ∧ qa u = b ∧ [[qn qd u ∧ a = b] 
∨ isvertex qad u ∧ path[a, qad u, qd u]]]⊗

⊗path gives the criterion for a list ⊗u to represent a path from ⊗a to ⊗b in G.
.nofill

	⊗⊗∀a b n: [gamma [a, b, n] ≡ [n=0 ∧ a=b] ⊗
			⊗⊗∨ [∃c: [gamma[a, c, n-1] ∧ a ε successors c] ⊗
			⊗⊗∧ ∀m: [m < n ⊃ ¬gamma[a, b, m]]]]⊗

		
	⊗⊗∀a b: [incomponent[a, b] ≡ ∃u: path[a, b, u]]⊗

.fill
By induction on ⊗n one can prove

	(i) ⊗⊗∀a b n: [gamma[a, b, n] ⊃ ∃u: [path[a, b, u] ∧ length u = n+1]]⊗

By induction on ⊗⊗length u⊗ one can prove

	(ii) ⊗⊗∀a b u: [path[a, b, u] ⊃ ∃n: [n<length u ∧ gamma[a, b, n]]]⊗

From (i) and (ii) we conclude that

	(iii) ⊗⊗∀a b: [∃u: path[a, b, u] ≡ ∃n: gamma[a, b, n]]⊗

and hence

	(iv) ⊗⊗∀a b: [incomponent[a, b] ≡ ∃n: gamma[a, b, n]]⊗

Now we wish to define a function ⊗component on vertices such that

	(v) ⊗⊗∀a b: [b ε component[a] ≡ ∃n: gamma [a, b, n]]⊗


For the present we assume that finiteness of the graph G means

FIN	⊗⊗∀a: ∃l: ∀m: [[m≥l ⊃ ∀b: ¬gamma[a, b, l]] ∧ [m<l ⊃ ∃b: gamma[a, b, m]]]⊗

Define the function computing the component of a vertex as follows (assume ⊗seen is
of sort list)


	⊗⊗∀a: [component a = comp[<a>, qNIL]]⊗

	⊗⊗∀u seen: [comp[u,seen] = qif qn u qthen seen qelse comp[gam[u]~seen, u*seen]]⊗

	⊗⊗∀u: [gam[u] = qif qn u qthen qNIL qelse successors qa u * gam[qd u]]⊗

We now show ⊗⊗∀a: islist component a⊗  and
⊗⊗∀a b: [b ε component a ≡ incomponent[a, b]]⊗.  This is done by
using CVI induction with 
.nofill

	⊗⊗qP(n) ≡ ∀u seen: [[∀b: [b ε u ≡ gamma[a, b, N-n]] ⊗
		    ⊗⊗∧ ∀b: [b ε seen ≡ ∃m: m<N-n ∧ gamma[a, b, m]]]⊗
			⊗⊗⊃ islist comp[u, seen] ∧ ∀b: [b ε comp[u, seen] ≡ ∃n: gamma[a, b, n]]]⊗
.fill

where ⊗N is the bound guaranteed by FIN.
Briefly this goes as follows.  In the case n=0, using FIN we have ⊗u = qNIL 
and by the hypothesis on ⊗seen the result follows.  If ⊗n>0  then by FIN ⊗u ≠ qNIL
so ⊗comp[u,seen] reduces to ⊗⊗comp[gam[u]~seen,_u*seen]⊗.  With n1=n-1 we have

	⊗⊗∀b: [b ε gam[u]~seen ≡ gamma[a, b, N-n1]]⊗

	⊗⊗∀b: [b ε u*seen ≡ ∃m: m<N-n1 ∧ gamma[a, b, m]]⊗

using properties of ⊗u, ⊗seen, and the definitions of ⊗gam and ⊗gamma and so the
conclusion of qP holds.

	Finally with ⊗n=N and ⊗u=<a> and ⊗⊗seen=qNIL⊗ the hypothesis of qP is 
satisfied so we obtain the desired result using the definition of ⊗component.  

.bb Comments.

	Some fixing has to be done to deal with the predicate definitions.  In fact
it would probably be easier to replace ⊗gamma by a function that computes the 
corresponding set.   One is also likely to have to fuss with the free variable 
⊗a in the induction predicate to make FOL happy.
.bb Revised description of a possible solution to the "component of a graph" problem.

	Assume the function ⊗successors represents a finite graph G.  We introduce
a sort ⊗isvertex intended to test if an individual is a vertex in G,
and let the variables ⊗a, ⊗b, ⊗c ... range over vertices of G.
We define some properties useful in discussing graphs.

⊗⊗∀a b u: [path[a, b, u] ≡ ¬qn u ∧ qa u = b ∧ [[qn qd u ∧ a = b] 
∨ isvertex qad u ∧ path[a, qad u, qd u]]]⊗

⊗path gives the criterion for a list ⊗u to represent a path from ⊗a to ⊗b in G.

⊗⊗⊗∀w: [pathlength w = length w - 1]⊗

⊗pathlength is the length of the path represented by ⊗w.  

⊗⊗⊗∀a l: [depth a = l ≡ [∃b w: [pathlength w = m ∧ path[a, b, w]] ≡ m < l]]⊗

⊗depth gives the maximum distance from a given vertex to any connected vertex.
 The fact that G is finite tells us that ⊗depth is defined for any vertex of G.
Thus we have

$FIN	⊗⊗⊗∀a: ∃l: depth a =l⊗

The condition that a vertex ⊗b is the component of ⊗a (eg. ⊗b is connected to
⊗a is given by the predicate ⊗incomponent which is defined by

⊗⊗⊗∀a b:  [incomponent[a, b] ≡ ∃w: path[a, b, w]]⊗

We define a function to compute the set of vertices in the component of a given
vertex by

⊗⊗⊗∀a: [component a = comp[<a> qNIL]]⊗

⊗⊗⊗∀u seen: [comp[u,seen] = qif qn u qthen seen qelse comp[slist u - u*seen , u*seen]]⊗

⊗⊗⊗∀u: [slist u = qif qn u qthen qNIL qelse [successors qa u] ∪ [slist qd u]]⊗

We would like to show that ⊗component is correct, namely that

⊗⊗⊗∀a b: [b ε component a ≡ incomponent[a, b]]⊗

to do this we prove something about ⊗comp namely ⊗⊗∀n: qP[n]⊗

.nofill

⊗⊗∀a u seen:[[ n≤depth a ∧ qP1[a, u, seen] ∧ qP2[a, u, seen]]⊗
		⊗⊗ ⊃ [islist comp[u, seen] ∧ ∀b: [bεcomp[u,seen] ≡ incomponent[a,b]]]]⊗
.fill	

where

⊗⊗⊗qP1[n, a, u, seen] ≡ ∀b: [b ε seen ≡ ∃w: [plength w + n < depth a ∧ path[a, b, w]]]]⊗

⊗⊗⊗qP2[n, a, u, seen] ≡ ∀b: [b ε u ≡ ¬[b ε seen] ∧ ∃w: [plength w + n = depth a 
∧ path[a, b, w]]]⊗


Clearly if we take ⊗⊗n_=_depth_a⊗, ⊗u_=_<a>⊗ and ⊗⊗seen_=_qNIL⊗ then 
the hypotheses of qP are satisified and this proves what we wish to prove.

To prove qP we proceed by induction on ⊗n  There are 2 cases, ⊗⊗qn u⊗ and 
⊗¬qn u⊗.